
\section{Conclusion}\label{sec:conclusion}

In this paper, we defined conditions under which behavioral models developed
iteratively preserve the satisfaction of requirements from a previous version.
That is, given a model satisfying a set requirements, an evolved version of that
model will still satisfy those requirements as long as the evolution satisfies
the conditions specified in definition~\ref{def:AHL_morph_strength}. The
confidential filesystem case study showed how the formal theory can
assist iterative modeling in an automated way.

We plan on further investigating this research topic along two axis: extending
to other formalisms and extending other property classes. For the first
extension, we realize that our approach is currently restrained to behavioral
models expressible in APN. We are currently working on applying the
property-preserving evolution conditions on models at a higher-level of
abstraction, such as Statecharts. A preliminary work~\cite{Lucio2011}
transforming Statecharts to APN will help applying the iterative requirement
satisfaction on non-APN models. For the second extension, we have focused on
safety properties in this paper. We would like to investigate how other types of properties can be preserved during evolution, such as some reachability
properties.

%We have presented a preliminary study on the conditions necessary to implement
%automatically assisted model evolution. We are conscious of the fact that our
%study only focuses on a particular kind of properties and
%domain of application. However, the alternative of performing such a study in a
%domain independent fashion is most likely restricted to theoretical
%considerations. For the future we consider relaxing the evolution conditions
%presented here and researching property-preserving evolution conditions
%for other domains of application.

